#include <iostream>

#include "atom.h"
#include "bind.h"
#include "bytecode.h"
#include "configuration.h"
#include "coroutine.h"
#include "generalizer.h"
#include "node.h"
#include "predicates.h"
#include "system.h"
#include "tree.h"
#include "tuple.h"

std::multimap<Prototype, ProverFactoryBase*> *Prover::proversMap = 0;
std::multimap<Prototype, ProverFactoryBase*> *Prover::varArgsProversMap = 0;

bool OnceProver::prove () {
  if(!proved) {
    proved = true;
    return proveOnce ();
  } else
    return false;
}

bool OnceBindProver::prove () {
  if(!proved) {
    binder.capture (system->trail);
    if(proveOnce ())
      return proved = true;
  }

  binder.undo (system->trail);
  return false;
}

class PredicateProver : public Prover {
public:

  // We would manage to delete the rules iterator object
  PredicateProver (Prototype &proto, Node &e, System &s) :
    state (0), toProve (&e), prover (0), system (s) {
    rulesIterator = system.rules.createIterator (proto);
    if(!rulesIterator->valid ())
      std::cerr << "[WARNING] Undefined invocation pattern: " << e.dump ()
          << std::endl;
  }

  ~PredicateProver () {
    if(prover)
      delete prover;
    if(rulesIterator)
      delete rulesIterator;
  }

  bool isCut (Node *node, pNode &left, pNode &right) { // node must be final
    if(typeid(*node) == typeid(Tree)) {
      Tree &tree = static_cast<Tree&> (*node);
      if(tree.ops[0] == '!' && !tree.ops[1]) {
        left = tree.left;
        right = tree.right;
        return true;
      }
    }
    return false;
  }

  bool prove () {
    Tree *tree;
    Node *rule;
    pNode clause, nodeBeforeCut;

    crBegin;
    afterCut = false;

    // Match with rules one by one
    for(; rulesIterator->valid (); rulesIterator->next ()) {
      rule = **rulesIterator;
      generalized = generalize (*rule);
      binder.capture (system.trail);

      if(typeid(*generalized.node) == typeid(Tree)) {
        tree = static_cast<Tree*> ((Node*) generalized);

        if(equalOp(tree->ops, inferenceOperator)) { // An inference rule

          if(binder.bind (*toProve, *tree->left.node, system.trail)) {
            clause = tree->right.final ();

            // Process everything before cut commands first
            while(isCut (clause, nodeBeforeCut, clause)) {
              prover = Prover::create (*nodeBeforeCut, system);
              bool result = prover->prove ();
              delete prover;
              prover = 0;

              if(!result) goto fail;
              afterCut = true;
            }

            // Prolog people are logic people, aren't we?
            prover = Prover::create (*clause, system);
            while(prover->prove ()) crReturn(true);
            delete prover;
            prover = 0;

            fail:

            // We may have crReturn-ed. Reload local variables
            rule = **rulesIterator;

            binder.undo (system.trail);
            if(afterCut) goto failAfterCut; // Cut - The point of no return
          }
        }
      }

      // A tautological fact
      if(binder.bind (*toProve, *generalized, system.trail)) {
        crReturn(true);
        binder.undo (system.trail);
      }
    }

    crEnd;

    failAfterCut:
    delete rulesIterator;
    rulesIterator = 0;
    return false; // No match, failure
  }

  int state;
  pNode toProve, generalized;
  Prover *prover;
  System &system;
  RulesIterator *rulesIterator;
  Binder binder;
  bool afterCut;
};

class fail : public Prover {
predicateName("fail")

  bool prove () {
    return false;
  }
};

ProverFactoryRegistrar<fail, Atom::ID> failRegistrar;

class nl : public OnceProver {
predicateName("nl")

  bool proveOnce () {
    std::cout << std::endl;
    return true;
  }
};

ProverFactoryRegistrar<nl, Atom::ID> nlRegistrar;

// Use a binding prover to rollback binded variables
class notCall : public OnceBindTupleProver {
predicateName("not")

  notCall () :
    prover (0) {
  }
  ~notCall () {
    if(prover)
      delete prover;
  }

  bool proveOnce () {
    pNode toProve = excludeFirst (*tuple);
    prover = Prover::create (*toProve, *system);
    bool ret = prover->prove ();
    return !ret;
  }

  Prover *prover;
};

ProverFactoryRegistrar<notCall, Tuple::ID> notRegistrar;

// We have to inherit a binding prover since once may execute binding actions;
//  those have to be rolled back during backtracking
class once : public OnceBindTupleProver {
predicateName("once")

  once () :
    prover (0) {
  }
  ~once () {
    if(prover)
      delete prover;
  }

  bool proveOnce () {
    binder.capture (system->trail);
    pNode toProve = excludeFirst (*tuple);
    prover = Prover::create (*toProve, *system);
    bool ret = prover->prove ();
    return ret;
  }

  Prover *prover;
};

ProverFactoryRegistrar<once, Tuple::ID> onceRegistrar;

class repeat : public Prover {
predicateName("repeat")

  bool prove () {
    return true;
  } // Ever be true
};

ProverFactoryRegistrar<repeat, Atom::ID> repeatRegistrar;

class selectCall : public Prover {
predicateName("select")

  selectCall () :
    selecting (1), prover (0) {
  }
  ~selectCall () {
    if(prover)
      delete prover;
  }

  bool prove () {
    if(!prover)
      binder.capture (system->trail);

    while(!prover && selecting < tuple->nodes.size ()) {
      Node &selected = *tuple->nodes[selecting].final ();

      // Identifies whether it is an if-then clause
      if(typeid(selected) == typeid(Tree)) {
        Tree &tree = static_cast<Tree&> (selected);
        if(equalOp(tree.ops, selectIfOperator)) {
          prover = Prover::create (*tree.left, *system);
          bool condition = prover->prove ();
          delete prover;
          prover = 0;

          if(condition) // If if OK, then do then
            prover = Prover::create (*tree.right, *system);
          goto nextSelection;
        }
      }

      // Or a default choice
      prover = Prover::create (selected, *system);
      nextSelection: selecting++;
    }

    if(prover && prover->prove ())
      return true;
    else {
      binder.undo (system->trail);
      return false;
    }
  }

  unsigned int selecting; // List node being selected now
  Binder binder;
  Prover *prover; // then-clause to be proved
  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<selectCall, Tuple::ID, 0> selectRegistrar;

class yes : public OnceProver {
predicateName("yes")

  bool proveOnce () {
    return true;
  }
};

ProverFactoryRegistrar<yes, Atom::ID> yesRegistrar;

class nil : public yes { // Nil atom would success
predicateName("")
  ;
};

ProverFactoryRegistrar<nil, Atom::ID> nilRegistrar;

// After yes defined
class ifCall : public Prover {
predicateName("if")

  ifCall () :
    prover (0) {
  }
  ~ifCall () {
    if(prover)
      delete prover;
  }

  bool prove () {
    if(!prover) {
      binder.capture (system->trail);

      prover = Prover::create (*tuple->nodes[1], *system);
      bool condition = prover->prove ();
      delete prover;
      prover = 0;

      // Verify the then/else words - if you want
      int size = tuple->nodes.size ();
      /*if(size != 4 && size != 6)
       return false;
       Node &thenFinal = *tuple->nodes[2].final ();
       if(typeid(thenFinal) != typeid(Atom) ||
       static_cast<Atom&> (thenFinal).name != "then")
       return false;
       if(size == 6) {
       Node &elseFinal = *tuple->nodes[4].final ();
       if(typeid(elseFinal) != typeid(Atom) ||
       static_cast<Atom&> (elseFinal).name != "else")
       return false;
       }*/

      if(condition)
        prover = Prover::create (*tuple->nodes[3], *system);
      else if(size == 6)
        prover = Prover::create (*tuple->nodes[5], *system);
      else
        prover = new yes;
    }

    if(!prover->prove ()) {
      binder.undo (system->trail);
      return false;
    } else
      return true;
  }

  Binder binder;
  Prover *prover; // then- or else-clause to be proved
  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<ifCall, Tuple::ID, 0> ifRegistrar;

class LogicalAND : public Prover {
predicateName(",")

  LogicalAND () :
    state (0), proveLeft (0), proveRight (0) {
  }
  ~LogicalAND () {
    if(proveLeft)
      delete proveLeft;
    if(proveRight)
      delete proveRight;
  }

  bool prove () {
    crBegin;

    proveLeft = Prover::create (*tree.node->left, *system);
    while(proveLeft->prove ()) {
      proveRight = Prover::create (*tree.node->right, *system);
      while(proveRight->prove ())
      crReturn(true);
      delete proveRight;
      proveRight = 0;
    }
    delete proveLeft;
    proveLeft = 0;

    crEnd;
    return false;
  };

  int state;
  ReferenceCountedPointer<Tree> tree;
  System *system;
  Prover *proveLeft, *proveRight;
  void set (Tree &t, System &s) {tree = &t; system = &s;}
};

ProverFactoryRegistrar<LogicalAND, Tree::ID> logicalANDregistrar;

class LogicalOR : public Prover {
predicateName(";")

  LogicalOR () :
    state (0), prover (0) {
  }
  ~LogicalOR () {
    if(prover)
      delete prover;
  }

  bool prove () {
    crBegin;

    prover = Prover::create (*tree.node->left, *system);
    while(prover->prove ()) crReturn(true);
    delete prover;

    prover = Prover::create (*tree.node->right, *system);
    while(prover->prove ()) crReturn(true);

    crEnd;
    return false;
  };

  int state;
  ReferenceCountedPointer<Tree> tree;
  System *system;
  Prover *prover;
  void set (Tree &t, System &s) {tree = &t; system = &s;}
};

ProverFactoryRegistrar<LogicalOR, Tree::ID> logicalORregistrar;

ProverFactoryBase *Prover::findSystemPredicate (const Prototype &proto) {
  Prover::ProversMap::iterator iter = proversMap->find (proto);
  if(iter != proversMap->end ())
    return (*iter).second;

  if(proto.type == Tuple::ID) {
    Prototype proto1 = proto;
    proto1.u.length = 0;
    iter = varArgsProversMap->find (proto1);
    if(iter != varArgsProversMap->end ())
      return (*iter).second;
  }

  return 0;
}

// node must be final
Prover *Prover::createSystemPredicate (ProverFactoryBase *factory, Node &node,
    System &system) {
  Prover *ret = factory->instantiate ();

  if(typeid(node) == typeid(Atom))
    ret->set (static_cast<Atom&> (node), system);
  else if(typeid(node) == typeid(Tuple)) {
    Tuple &tuple = static_cast<Tuple&> (node);
    unsigned int factoryClauseLength = factory->clauseLength;
    if(factoryClauseLength == 0 || factoryClauseLength == tuple.nodes.size ())
      ret->set (tuple, system);
    else {
      delete ret; // Wrong number of parameters, fake
      ret = 0;
    }
  }
  else if(typeid(node) == typeid(Tree))
    ret->set (static_cast<Tree&> (node), system);
  else
    ret = 0;

  return ret;
}

Snippet *Prover::getSnippet (Prototype &proto, Node &node, System &system) {
  Snippet *snippetPointer = &system.rules.findSnippet (proto);

  if(!snippetPointer && system.rules.bytecodeEnabled) {

    // Ignores complicated prototype like ((func .closure) .arg)
    Snippet snippet;
    if(proto.type != Tuple::ID || proto.u.length == 0 ||
        static_cast<Tuple&> (node).nodes[0].final () == proto.functor)
      if(compileExecuteBytecode (proto, snippet, system))
        snippetPointer = &system.rules.putSnippet (proto, snippet);
  }

  return snippetPointer;
}

Prover *Prover::create (Node &node, System &system) {
  Node *finalNode = node.final (); // Good to ensure this
  Prototype proto = Prototype::get (*finalNode);

#if defined(trace)
  std::cerr << "[TRACE] " << node.display (0) << std::endl;
#endif

  // Checks if it is a system predicate
  ProverFactoryBase *factory = findSystemPredicate (proto);
  if(factory)
    return Prover::createSystemPredicate (factory, *finalNode, system);

  // Checks if there is byte-code, or compiles the predicate if option enabled
  Snippet *snippetPointer = getSnippet (proto, *finalNode, system);

  if(snippetPointer) // Runs byte-code if already compiled
    return new BytecodeExecutor (*snippetPointer, *finalNode, system);
  else
    // Prove it using rules
    return new PredicateProver (proto, *finalNode, system);
}
